app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
↳ QTRS
↳ Overlay + Local Confluence
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(id, x0)
app(add, 0)
app(app(add, app(s, x0)), x1)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
APP(app(add, app(s, x)), y) → APP(app(add, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))
APP(app(add, app(s, x)), y) → APP(s, app(app(add, x), y))
APP(app(add, app(s, x)), y) → APP(add, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(cons, app(f, x))
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(id, x0)
app(add, 0)
app(app(add, app(s, x0)), x1)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
APP(app(add, app(s, x)), y) → APP(app(add, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))
APP(app(add, app(s, x)), y) → APP(s, app(app(add, x), y))
APP(app(add, app(s, x)), y) → APP(add, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(cons, app(f, x))
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(id, x0)
app(add, 0)
app(app(add, app(s, x0)), x1)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
APP(app(add, app(s, x)), y) → APP(app(add, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))
APP(app(add, app(s, x)), y) → APP(s, app(app(add, x), y))
APP(app(add, app(s, x)), y) → APP(add, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(cons, app(f, x))
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(id, x0)
app(add, 0)
app(app(add, app(s, x0)), x1)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
APP(app(add, app(s, x)), y) → APP(app(add, x), y)
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(id, x0)
app(add, 0)
app(app(add, app(s, x0)), x1)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(add, app(s, x)), y) → APP(app(add, x), y)
s > add > app2 > APP1
s > add > app2 > id
0 > id
APP1: [1]
app2: [2,1]
id: multiset
0: multiset
s: multiset
add: multiset
app(add, 0) → id
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(id, x0)
app(add, 0)
app(app(add, app(s, x0)), x1)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(id, x0)
app(add, 0)
app(app(add, app(s, x0)), x1)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
Used ordering: Combined order from the following AFS and order.
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app2 > APP1 > map
cons > APP1 > map
APP1: [1]
map: multiset
app2: [1,2]
cons: multiset
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(id, x0)
app(add, 0)
app(app(add, app(s, x0)), x1)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
map > APP2 > app2
cons > APP2 > app2
map: multiset
app2: [2,1]
APP2: [1,2]
cons: multiset
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(id, x0)
app(add, 0)
app(app(add, app(s, x0)), x1)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))